Nuprl Lemma : inl-do-apply
11,40
postcript
pdf
A
,
B
:Type,
f
:(
A
(
B
+ Top)),
x
:
A
. (
can-apply(
f
;
x
))
((inl do-apply(
f
;
x
) ) ~ (
f
(
x
)))
latex
ProofTree
Definitions
False
,
t
T
,
P
Q
,
b
,
True
,
left
+
right
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
s
=
t
,
Top
,
f
(
a
)
,
do-apply(
f
;
x
)
,
can-apply(
f
;
x
)
,
Type
Lemmas
true
wf
,
false
wf
origin
A, B:Type, f:(A
(B + Top)), x:A. (
can-apply(f;x)) 
((inl do-apply(f;x) ) ~ (f(x)))
A, B:Type, f:(A(B + Top)), x:A. (can-apply(f;x)) ((inl do-apply(f;x) ) ~ (f(x)))
T QbB(x)x:A. B(x)